
-- kind Nat = Z | S Nat deriving Singleton Nat'
-- data Equal:: * ~> * ~> * where Eq:: Equal a a 


plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}  -- deriving Relation Plus

plusZ :: Nat' n -> Equal {plus n Z} n
plusZ Z = Eq
plusZ (x@(S m)) = Eq
  where theorem indHyp = plusZ m
         
plusS :: Nat' n -> Equal {plus n (S m)} (S{plus n m})
plusS Z  = Eq
plusS (S x)  = Eq
  where theorem ih = plusS x
        
        
plusCommutes :: Nat' n -> Nat' m -> Equal {plus n m} {plus m n}
plusCommutes Z m = Eq
   where theorem lemma = plusZ m
plusCommutes (S x) m = Eq
   where theorem plusS,
                 indHyp = plusCommutes x m
         
--------------------------------------------
-- Relational versions

data Plus:: Nat ~> Nat ~> Nat ~> *0 where
  Plus0 :: Plus Z m m
  Plus1 :: Plus n m c -> Plus (S n) m (S c)

pluS:: Plus a b c -> Plus a (S b) (S c)
pluS Plus0 = Plus0
pluS (Plus1 p) = Plus1(pluS p)

plusCom:: Nat' b -> Plus a b c -> Plus b a c
plusCom Z Plus0 = Plus0
plusCom (S n) Plus0 = Plus1(plusCom n Plus0)
plusCom Z (Plus1 p) = pluS(plusCom Z p)
plusCom (S n) (Plus1 p) = pluS(plusCom (S n) p)

trans:: Plus a b c -> Equal {plus a b} c
trans Plus0 = Eq
trans (Plus1 p) =  Eq
  where theorem indHyp = trans p

transInv :: Nat' a -> Equal {plus a b} c -> Plus a b c
transInv Z Eq = Plus0
transInv (x@(S n)) (p@Eq) = Plus1(transInv n Eq)

funcDepend:: (Plus a b c,Plus a b d) -> Equal c d
funcDepend (Plus0,Plus0) = Eq
funcDepend (Plus0,Plus1 p) = unreachable
funcDepend (Plus1 p,Plus0) = unreachable
funcDepend (Plus1 p,Plus1 q) = 
   case funcDepend(p,q) of
     (Eq) -> Eq

-------------------------------------   
{-
Reg w v

rippleCarryAdder:: Reg w v -> Reg w u -> Reg (S w) {plus u v}

-}